Issue2067b.agda:21,7-8
Nat !=< M.A n of type Set
when checking that the expression n has type M.A n
